e:s.P(s)@j 
== (x:Id. vartype(j;x)  ds(x)?Top)
== & e'@j. (e' < e)  P(state after e')  (e'':E. (e' <loc e'') & (e' < e))
== & & e'@j. (e < e')  P((state when e'))  (e'':E. (e'' <loc e') & (e < e')) 

latex

---

clarification:

es-simul(es;e;j;ds;s.P(s))
== (x:Id. es-vartype(es; j; x)  fpf-cap(ds;IdDeq;x;Top))
== & alle-at(es;j;e'.es-causl(es; e'; e)
== & alle-at(es;j;e'. P(es-state-after(es;e'))
== & alle-at(es;j;e'.  (e'':es-E(es). es-locl(es; e'; e'') & es-causl(es; e'; e)))
== & & alle-at(es;j;e'.es-causl(es; e; e')
== & & alle-at(es;j;e'. P(es-state-when(es;e'))
== & & alle-at(es;j;e'.  (e'':es-E(es). es-locl(es; e''; e') & es-causl(es; e; e'))) 

latex

Definitions	A & B, x:A. B(x), Id, vartype(i;x), f(x)?z, IdDeq, Top, state after e, e@i. P(e), P  Q, P  Q, (state when e), x:A. B(x), E, P & Q, (e <loc e'), (e < e')
FDL editor aliases	es-simul